module Parser where

import Data.Array
import Data.List
import Lexer
import ModelChecker
import DirectApproach
  
-- Function that takes a list of tokens and return the corresponding HMM  
parse :: [Token] -> HMM Int 
parse t = createHMM t dummyHMM
  where dummyHMM = HMM {statesHMM = array (0,0) [(0,-1)],
                        pTransHMM = array ((0,0),(0,0)) [((0,0),-1)],
                        labelFHMM = array (0,0) [(0,[""])],
                        obsHMM = "",
                        pObsHMM = array ((0,0),(0,0)) [((0,0),-1)],
                        initDiHMM = array (0,0) [(0,-1.0)]}
                
-- This auxiliary function takes three by three tokens with which a                    
-- new element of the HMM is made up
createHMM :: [Token] -> HMM Int -> HMM Int
createHMM [] hmm = hmm
createHMM ((Rsv St): ODef : (SetSt n):moreTokens) hmm 
  | n <= 0 = error "The number of states must be a positive integer."
  | otherwise = createHMM moreTokens newHMM
  where
    newHMM = HMM {statesHMM = listArray (1,n) [1..n],
                    pTransHMM = pTransHMM hmm,                
                    labelFHMM = labelFHMM hmm,                
                    obsHMM = obsHMM hmm,                
                    pObsHMM = pObsHMM hmm,                
                    initDiHMM = initDiHMM hmm}
createHMM ((Rsv Trans): ODef : (ListFloat lstFloat):moreTokens) hmm 
  | length lstFloat /= n*n = error "Error parsing the transition probability matrix. The size of the matrix is not correct."             
  | not (sumOne lstFloat n) = error "Error parsing the transition probability matrix. Some row does not sum up to 1."     
  | otherwise = createHMM moreTokens newHMM 
  where
    st = statesHMM hmm
    newHMM = HMM {statesHMM = st,
                    pTransHMM = listArray ((1,1),(n,n)) lstFloat,                
                    labelFHMM = labelFHMM hmm,                
                    obsHMM = obsHMM hmm,                
                    pObsHMM = pObsHMM hmm,                
                    initDiHMM = initDiHMM hmm}
    n = rangeSize (bounds st)
createHMM ((Rsv Lbl): ODef : (ListAtom lstAtom):moreTokens) hmm 
  | length lstAtom /= n = error "Error parsing the labels. The number of lists of strings does not corresponds to the number of states."
  | otherwise = createHMM moreTokens newHMM 
  where
    st = statesHMM hmm
    newHMM = HMM {statesHMM = st,
                    pTransHMM = pTransHMM hmm,                
                    labelFHMM = listArray (1,n) lstAtom,                
                    obsHMM = obsHMM hmm,                
                    pObsHMM = pObsHMM hmm,                
                    initDiHMM = initDiHMM hmm}
    n = rangeSize (bounds st)
createHMM ((Rsv Obs): ODef : (SetObs obs):moreTokens) hmm = createHMM moreTokens newHMM 
  where        
    newHMM = HMM {statesHMM = statesHMM hmm,
                  pTransHMM = pTransHMM hmm,                
                  labelFHMM = labelFHMM hmm,                
                  obsHMM = obs,                
                  pObsHMM = pObsHMM hmm,                
                  initDiHMM = initDiHMM hmm}
createHMM ((Rsv ObsProb): ODef : (ListFloat lstFloat):moreTokens) hmm 
  | length lstFloat /= n*m =  error "Error parsing the observation probability matrix. Inadequate matrix size."
  | not (sumOne lstFloat m) =  error "Error parsing the observation probability matrix. No all of the rows of the matrix sum up to 1."
  | otherwise = createHMM moreTokens newHMM
  where
    st = statesHMM hmm
    obs = obsHMM hmm
    newHMM = HMM {statesHMM = st,
                  pTransHMM = pTransHMM hmm,                
                  labelFHMM = labelFHMM hmm,                
                  obsHMM = obs,                
                  pObsHMM = listArray ((1,1),(n,m)) lstFloat,                
                  initDiHMM = initDiHMM hmm}
    n = rangeSize (bounds st)
    m = length obs
createHMM ((Rsv IniDist): ODef : (Lista lstInitial):moreTokens) hmm 
  | length lstInitial /= n = error "Error parsing the initial distribution. The initial distributions list size is wrong." 
  -- | not (sumOne lstInitial n) = error "Error parsing the initial distribution. The initial distribution does not sum up to 1."
  | otherwise = createHMM moreTokens newHMM  
  where
    st = statesHMM hmm
    newHMM = HMM {statesHMM = st,
                    pTransHMM = pTransHMM hmm,                
                    labelFHMM = labelFHMM hmm,                
                    obsHMM = obsHMM hmm,                
                    pObsHMM = pObsHMM hmm,                
                    initDiHMM = listArray (1,n) lstInitial}
    n = rangeSize (bounds st)
createHMM _ hmm = error "Error parsing unkown token."

-- This function takes a list a float numbers and 
sumOne [] _ = True
sumOne lst size = ((sum elemLst) == 1) && (sumOne rest size)
  where
    (elemLst, rest) = splitAt size lst
    
-- Given a list of TknPOCTLs returns the well formed POCTL* function.
-- Notice the use of the auxiliaty function parsePhi. The grammar used  
-- in this parser models the precedence of operators and is shown below:
--      Phi ::= Psi | Psi v Phi
--      Psi ::= Theta | Theta ^ Psi
--      Theta ::= True | False | a | ~Theta | (Phi) | P [comp x] A
-- where A is a path formula obtained by the grammar
--      A ::= B | B v A
--      B ::= C | C ^ B
--      C ::= D | D U C
--      D ::= E | E U n D
--      E ::= ~E | (A) | X_{obs} E | Phi
parsePOCTL :: [TknPOCTL] -> POCTL
parsePOCTL xs =
  case (parsePhi xs) of
    (formula, []) -> formula
    _             -> error "Parsing failed!"
    
-- This function parses the grammatical cathegory Phi ::= Psi | Psi v Phi
parsePhi :: [TknPOCTL] -> (POCTL, [TknPOCTL])
parsePhi tkns = 
  case rec of
    (LogOp Disj):left   -> let (phi, rmndr) = parsePhi left 
                           in (OP psi phi, rmndr)
    _                   -> (psi, rec) 
  where
    (psi, rec) = parsePsi tkns
    
-- This function parses the grammatical cathegory Psi ::= Theta | Theta ^ Psi
parsePsi :: [TknPOCTL] -> (POCTL, [TknPOCTL])
parsePsi tkns =
  case rec of
    (LogOp Conj):left   -> let (psi, rmndr) = parsePsi left                   
                           in (YP theta psi, rmndr)
    _                   -> (theta, rec) 
  where
    (theta, rec) = parseTheta tkns
    
-- This function parses the grammatical cathegory Theta ::= True | False | a | ~Theta | (Phi) | P [comp x] A
parseTheta :: [TknPOCTL] -> (POCTL, [TknPOCTL])
parseTheta (Ttrue:tkns)     = (VerdadP, tkns)
parseTheta (Ffalse:tkns)    = (FalsoP, tkns)
parseTheta (AProp str:tkns) = (AtomP str, tkns)
parseTheta (LeftPar:tkns)   = let (phi, left) = parsePhi tkns 
                              in case left of
                                (RightPar:rmndr) -> (phi, rmndr)
                                _                -> error "Failure since there is a missing closing parenthesis"
parseTheta (LogOp Neg:tkns) = let (theta, left) = parseTheta tkns 
                              in (NoP theta, left)                               
parseTheta (ProbOp
            :LeftSqBrckt
            :Comp c
            :Range x
            :RightSqBrckt
            :tkns) = if 0<=x && x<=1 
                     then let (path, rmndr) = parsePathA tkns                                                                         
                          in (Prob c x path,rmndr) 
                     else error "The number that is used to define the probability range is not a number between 0 and 1."

-- Now, we will parse the path formulas according to the grammar 
--      A ::= B | B v A
--      B ::= C | C ^ B
--      C ::= D | D U C
--      D ::= E | E U n D
--      E ::= ~E | (A) | X_{obs} E | Phi
-- Next we'll parse the grammatical cathegory A ::= B | B v A 
parsePathA :: [TknPOCTL] -> (PathF, [TknPOCTL])
parsePathA tkns = 
  case xs of
    (LogOp Disj):left   -> let (a, rmndr) = parsePathA left 
                           in (OPath b a, rmndr)
    _                   -> (b, xs) 
  where
    (b, xs) = parsePathB tkns
    
-- Next we'll parse the grammatical cathegory B ::= C | C ^ B
parsePathB :: [TknPOCTL] -> (PathF, [TknPOCTL])
parsePathB tkns =
  case xs of
    (LogOp Conj):left   -> let (b, rmndr) = parsePathB left 
                           in (YPath c b, rmndr)
    _                   -> (c, xs) 
  where
    (c, xs) = parsePathC tkns
    
-- Next we'll parse the grammatical cathegory C ::= D | D U C
parsePathC :: [TknPOCTL] -> (PathF, [TknPOCTL])
parsePathC tkns = 
  case xs of 
    (TempOp UntilO):left        -> let (c, rmndr) = parsePathC left                            
                                   in (UntilPath d c, rmndr)
    _                           -> (d, xs) 
  where
    (d, xs) = parsePathD tkns
    
-- Next we'll parse the grammatical cathegory D ::= E | E U n D
parsePathD :: [TknPOCTL] -> (PathF, [TknPOCTL])
parsePathD tkns =
  case xs of
    (TempOp UntilO
     :UBound n
     :left)        -> if n >= 0 
                      then let (d, rmndr) = parsePathD left                                                          
                           in (UntilBPath n e d, rmndr) 
                      else error "The bounded until operator is bounded by a negative number."
    _              -> (e, xs) 
  where
    (e, xs) = parsePathE tkns

-- Next we'll parse the grammatical cathegory E ::= ~E | (A) | X_{obs} E | Theta
parsePathE :: [TknPOCTL] -> (PathF, [TknPOCTL])
parsePathE (LogOp Neg:tkns) = let (e,rmndr) = parsePathE tkns                        
                              in (NoPath e, rmndr)
parsePathE (LeftPar:tkns) = let (a, rmndr) = parsePathA tkns
                            in case rmndr of
                              (RightPar):xs     -> (a, xs)
                              _                 -> error "No closing parenthesis found."
parsePathE (TempOp NextO
            :Underscore
            :NextObs obs:tkns) = let (e, rmndr) = parsePathE tkns                                                        
                                 in (NextPath obs e, rmndr)
parsePathE tkns = let (theta, rmndr) = parseTheta tkns 
                  in (FormP theta, rmndr)